/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXI30/FONT#2=BAXB30/FONT#3=BAXS30/FONT#4=GACS25/FONT#5=CLAR30/FONT#8=SAIL25



␈↓ ↓N␈↓␈↓ ¬∞Research Proposal Submitted to


␈↓ ↓N␈↓␈↓ ∧-␈↓αTHE NATIONAL SCIENCE FOUNDATION


␈↓ ↓N␈↓α␈↓ εK␈↓for


␈↓ ↓N␈↓␈↓ ∧R␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence


␈↓ ↓N␈↓α␈↓ εN␈↓by


␈↓ ↓N␈↓␈↓ ¬wJohn McCarthy
␈↓ ↓N␈↓␈↓ ¬↔Professor of Computer Science
␈↓ ↓N␈↓␈↓ ¬QPrincipal Investigator








␈↓ ↓N␈↓␈↓ ε July 1977





␈↓ ↓N␈↓␈↓ ¬→Computer Science Department

␈↓ ↓N␈↓␈↓ ¬ ␈↓αSTANFORD UNIVERSITY

␈↓ ↓N␈↓α␈↓ ¬[␈↓Stanford, California



␈↓ ↓N␈↓¬␈↓ ↓YResearch Proposal Submitted to the National Science Foundation





␈↓ ↓N␈↓Proposed Amount ␈↓&␈↓λ$xx,xxx␈↓␈↓)αβ Proposed E␈↓λ␈↓β@␈↓λ␈↓ective Date ␈↓&␈↓λ1 Jan. 1978␈↓␈↓)αβ Proposed Duration ␈↓&␈↓λ3 years␈↓␈↓)αβ



␈↓ ↓N␈↓Title ␈↓&␈↓λBasic Research in Artificial Intelligence␈↓␈↓)αβ



␈↓ ↓N␈↓Principal Investigator ␈↓&␈↓λJohn McCarthy␈↓␈↓)αβ␈↓ ε>Submitting Institution ␈↓&␈↓λStanford University␈↓␈↓)αβ
␈↓ ↓N␈↓  Soc. Sec. No. ␈↓&␈↓λ558-30-4793␈↓␈↓)αβ␈↓ ε>Department ␈↓&␈↓λ Computer Science    ␈↓␈↓)αβ
␈↓ ↓N␈↓␈↓ ε>Address ␈↓&␈↓λStanford, California 94305␈↓␈↓)αβ



␈↓ ↓N␈↓Make grant to ␈↓&␈↓λBoard of Trustees of the Leland Stanford Junior University␈↓␈↓)αβ



␈↓ ↓N␈↓Endorsements:

␈↓ ↓N␈↓␈↓ α↑Principal Investigator␈↓ ¬nDepartment Head␈↓ λnInstitutional Admin. O␈↓λ␈↓β@␈↓λ␈↓icial

␈↓ ↓N␈↓Name␈↓ α↑␈↓&␈↓λJohn McCarthy        ␈↓␈↓)αβ␈↓ ¬n␈↓&␈↓λEdward A. Feigenbaum ␈↓␈↓)αβ␈↓ λ}␈↓&␈↓λ                     ␈↓␈↓)αβ


␈↓ ↓N␈↓Signature␈↓ α↑␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ ¬n␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ λ}␈↓&␈↓λ                     ␈↓␈↓)αβ

␈↓ ↓N␈↓Title␈↓ α↑␈↓&␈↓λProfessor            ␈↓␈↓)αβ␈↓ ¬n␈↓&␈↓λProfessor & Chairman ␈↓␈↓)αβ␈↓ λ}␈↓&␈↓λ                     ␈↓␈↓)αβ

␈↓ ↓N␈↓Telephone␈↓ α↑␈↓&␈↓λ(415) 497-4430       ␈↓␈↓)αβ␈↓ ¬n␈↓&␈↓λ(415) 497-4079       ␈↓␈↓)αβ␈↓ λ}␈↓&␈↓λ                     ␈↓␈↓)αβ

␈↓ ↓N␈↓Date␈↓ α↑␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ ¬n␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ λ}␈↓&␈↓λ                     ␈↓␈↓)αβ
␈↓ ↓N␈↓α␈↓ ε↑␈↓ b1


␈↓ ↓N␈↓α␈↓ βEAbstract                                    ␈↓ π∞␈↓The␈α∂lines␈α∂of␈α⊂research␈α∂we␈α∂plan␈α∂to␈α⊂pursue␈α∂are
                                            ␈↓ π∞␈↓exempli␈↓↓␈↓βC␈↓↓␈↓ed␈α≤in␈α≤the␈α≤attached␈α≤reprints␈α≠and
␈↓ ↓N␈↓This␈α⊃is␈α⊂a␈α⊃request␈α⊂for␈α⊃a␈α⊂grant␈α⊃in␈α⊃support␈α⊂of          ␈↓ π∞␈↓preprints.␈α∀ Here␈α∀we␈α∀shall␈α∀explain␈α∃how␈α∀this
␈↓ ↓N␈↓basic␈α⊗research␈α∃in␈α⊗arti␈↓βC␈↓cial␈α⊗intelligence␈α∃with    ␈↓ π∞␈↓work␈α∂␈↓↓␈↓βC␈↓↓␈↓ts␈α∂together.␈α∂ Our␈α∂long␈α∂range␈α∂goal␈α∂is␈α∞a
␈↓ ↓N␈↓emphasis␈αon␈αthe␈αstructure␈αof␈αformal␈αreasoning     ␈↓ π∞␈↓program␈α
that␈α
can␈α
be␈α
told␈α
facts␈α
about␈α
the␈α
world
␈↓ ↓N␈↓and␈α∞computer␈α∞proof␈α∞checking.␈α∞ The␈α
computer       ␈↓ π∞␈↓and␈α∩can␈α⊃use␈α∩them␈α⊃e␈↓↓␈↓β@␈↓↓␈↓ectively␈α∩to␈α∩achieve␈α⊃the
␈↓ ↓N␈↓proof␈α∞checking␈α
supports␈α∞the␈α
basic␈α∞research␈α
in     ␈↓ π∞␈↓goals␈α⊃it␈α∩is␈α⊃given.␈α⊃ Sometimes␈α∩it␈α⊃will␈α∩use␈α⊃the
␈↓ ↓N␈↓AI,␈α↔but␈α↔also␈α⊗has␈α↔applications␈α↔to␈α⊗verifying        ␈↓ π∞␈↓facts␈α∨directly␈α∨from␈α≡its␈α∨data␈α∨base␈α≡using
␈↓ ↓N␈↓computer␈α≡programs␈α≥and␈α≡is␈α≥independently          ␈↓ π∞␈↓deductive␈α↔and␈α↔inductive␈α↔processes␈α↔like␈α⊗the
␈↓ ↓N␈↓valuable.                                   ␈↓ π∞␈↓deductive␈α≠processes␈α≠of␈α≠mathematical␈α~logic.
                                            ␈↓ π∞␈↓However,␈α_we␈α_are␈α_already␈α_sure,␈α↔(McCarthy
␈↓ ↓N␈↓α␈↓ β)Introduction                                ␈↓ π∞␈↓1977a),␈α≠that␈α≠conjectural␈α≠processes␈α≠will␈α≠be
                                            ␈↓ π∞␈↓needed␈α∂that␈α∂go␈α∂beyond␈α∂deduction␈α∂as␈α∞preently
␈↓ ↓N␈↓Arti␈↓βC␈↓cial␈α→intelligence␈α→has␈α_proved␈α→to␈α→be␈α_a         ␈↓ π∞␈↓conceived.␈α Sometimes␈αit␈αwill␈αuse␈αthese␈αfacts␈αto
␈↓ ↓N␈↓di␈↓β@␈↓icult␈α≠branch␈α≤of␈α≠science.␈α≤ Some␈α≠people         ␈↓ π∞␈↓compile␈α"expert␈αprograms"␈αthat␈αuse␈αthese␈αfacts
␈↓ ↓N␈↓thought␈αthat␈αhuman␈α
level␈αintelligence␈αcould␈α
be    ␈↓ π∞␈↓in␈αa␈αmore␈αe␈↓↓␈↓β@␈↓↓␈↓icient␈αway␈αthan␈αsimple␈αreasoning.
␈↓ ↓N␈↓achieved␈α∞in␈α∞ten␈α∞or␈α∞twenty␈α∞years,␈α∞but␈α∞this␈α
was       ␈↓ π∞␈↓However,␈α∪the␈α∩expert␈α∪programs␈α∩will␈α∪have␈α∩to
␈↓ ↓N␈↓based␈α∂on␈α∞the␈α∂di␈↓β@␈↓iculties␈α∞they␈α∂could␈α∂see␈α∞when       ␈↓ π∞␈↓defer␈αto␈αreasoning␈αwhen␈αunexpected␈αuse␈αof␈αhe
␈↓ ↓N␈↓they␈α⊗made␈α⊗the␈α⊗optimistic␈α⊗predictions.␈α∃ Our       ␈↓ π∞␈↓factual data-base is required.
␈↓ ↓N␈↓own␈α
opinion␈αis␈α
that␈α
major␈αscienti␈↓βC␈↓c␈α
discoveries
␈↓ ↓N␈↓remain␈αto␈α
be␈αmade.␈α
 Moreover,␈αmany␈α
of␈αthese        ␈↓ π∞␈↓We␈α↔do␈α↔not␈α↔propose␈α↔to␈α↔implement␈α↔such␈α⊗a
␈↓ ↓N␈↓discoveries␈α∪require␈α∪theoretical␈α∀advances␈α∪and    ␈↓ π∞␈↓program␈α→immediately␈α→-␈α→maybe␈α→not␈α→at␈α→all
␈↓ ↓N␈↓not␈α∞merely␈α∂the␈α∞extension␈α∂of␈α∞current␈α∂ideas␈α∞for      ␈↓ π∞␈↓within␈αthe␈αnext␈α␈↓↓␈↓βC␈↓↓␈↓ve␈αyears.␈α This␈αis␈αbecause␈αits
␈↓ ↓N␈↓producing␈α
"expert␈α
programs"␈α
to␈α
new␈αdomains.      ␈↓ π∞␈↓success␈α
depends␈αon␈α
successful␈α
formalization␈αof
␈↓ ↓N␈↓The␈αincreasing␈αemphasis␈αby␈αARPA␈αand␈αother         ␈↓ π∞␈↓facts␈α≥about␈α≥the␈α≤world.␈α≥ We␈α≥have␈α≤made
␈↓ ↓N␈↓agencies␈αsponsoring␈αAI␈αresearch␈αon␈αimmediate     ␈↓ π∞␈↓progress␈α
in␈α
this␈α
formalization,␈α
but␈α
we␈α
may␈α
be
␈↓ ↓N␈↓applications␈α$has␈α$resulted␈α$in␈α%a␈α$serious           ␈↓ π∞␈↓occupied␈α
with␈α
it␈αexclusively␈α
for␈α
the␈αforseeable
␈↓ ↓N␈↓imbalance.␈α Deciding␈αwhat␈αthe␈αbasic␈αissues␈αare    ␈↓ π∞␈↓future.␈α In␈α
short␈αwe␈αwill␈α
emphasize␈αtheoretical
␈↓ ↓N␈↓is␈α⊂di␈↓β@␈↓icult␈α⊂enough␈α⊂without␈α⊃having␈α⊂formulate      ␈↓ π∞␈↓arti␈↓↓␈↓βC␈↓↓␈↓cial␈α∞intelligence␈α
except␈α∞for␈α
the␈α∞work␈α
with
␈↓ ↓N␈↓everything␈α*in␈α*terms␈α*of␈α)demonstration            ␈↓ π∞␈↓proof-checkers to be described beLow.
␈↓ ↓N␈↓programs to be available in two years.
                                            ␈↓ π∞␈↓The␈α0main␈α1areas␈α0of␈α1our␈α0previous
␈↓ ↓N␈↓Our␈α⊃research␈α∩is␈α⊃based␈α⊃on␈α∩the␈α⊃idea␈α∩that␈α⊃fkr          ␈↓ π∞␈↓accomplishment␈α~and␈α≠future␈α~work␈α≠are␈α~the
␈↓ ↓N␈↓many␈α~purposes,␈α≠the␈α~problems␈α≠of␈α~arti␈↓βC␈↓cial         ␈↓ π∞␈↓following (as now seen):
␈↓ ↓N␈↓intelligence␈α∞can␈α∞be␈α
separated␈α∞into␈α∞two␈α∞parts␈α
-
␈↓ ↓N␈↓an␈α⊂epistemological␈α⊂part␈α⊂and␈α⊂a␈α⊃heuristic␈α⊂part.     ␈↓ π∞␈↓1.␈α∂Development␈α∂of␈α∂␈↓↓circumscription␈↓␈α∂as␈α∂a␈α∂mode
␈↓ ↓N␈↓The␈α⊃␈↓↓epistemological␈↓␈α⊂part␈α⊃concerns␈α⊃what␈α⊂facts     ␈↓ π∞␈↓of␈α∩reasoning␈α∩and␈α∩its␈α∩application␈α∪to␈α∩arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓N␈↓and␈αinference␈αrules␈αare␈αavailable␈αfor␈αsolving␈αa    ␈↓ π∞␈↓intelligence.␈α~ ␈↓↓Circumscription␈↓␈α~formalizes␈α~the
␈↓ ↓N␈↓problem␈α∞and␈α∞how␈α∞they␈α∞can␈α∞be␈α∞represented␈α∞in         ␈↓ π∞␈↓process␈αof␈αconcluding␈α(often␈αincorrectly)␈αthat␈αa
␈↓ ↓N␈↓the␈α∞memory␈α∂of␈α∞a␈α∂computer,␈α∞and␈α∂the␈α∞heuristic        ␈↓ π∞␈↓certain␈α→collection␈α→of␈α~facts␈α→is␈α→all␈α~that␈α→are
␈↓ ↓N␈↓part␈αconcerns␈αprocedures␈αfor␈αdeciding␈α
what␈αto     ␈↓ π∞␈↓relevant␈α
for␈αsolving␈α
a␈α
problem.␈α It␈α
does␈αthis␈α
by
␈↓ ↓N␈↓do␈α∂on␈α∂the␈α∂basis␈α∂of␈α∂the␈α∂necessary␈α∂facts.␈α∞ Most       ␈↓ π∞␈↓allowing␈α_one␈α_to␈α↔formally␈α_assume␈α_that␈α↔the
␈↓ ↓N␈↓work␈α∞in␈α∞AI␈α
has␈α∞concerned␈α∞the␈α∞␈↓↓heuristics␈↓,␈α
and       ␈↓ π∞␈↓entitities␈α≥that␈α≡are␈α≥generated␈α≡by␈α≥speci␈↓↓␈↓βC␈↓↓␈↓ed
␈↓ ↓N␈↓computer␈α∞representations␈α
of␈α∞information␈α
have    ␈↓ π∞␈↓processes␈α∃are␈α∀all␈α∃the␈α∀entities␈α∃of␈α∃a␈α∀speci␈↓↓␈↓βC␈↓↓␈↓ed
␈↓ ↓N␈↓been␈α∂chosen␈α∂that␈α∂are␈α∂capable␈α∂of␈α∂representing      ␈↓ π∞␈↓kind.␈α⊃ This␈α∩is␈α⊃common␈α⊃in␈α∩human␈α⊃reasoning
␈↓ ↓N␈↓only␈α∞a␈α
part␈α∞of␈α
the␈α∞information␈α
that␈α∞would␈α
be        ␈↓ π∞␈↓and,␈α∀for␈α∃reasons␈α∀described␈α∀in␈α∃the␈α∀preprint,
␈↓ ↓N␈↓available␈α∨to␈α∨a␈α∨human.␈α∨ The␈α∨modes␈α≡of               ␈↓ π∞␈↓canot␈α≥be␈α≥accomplished␈α≥by␈α≥any␈α≥form␈α≥of
␈↓ ↓N␈↓reasoning␈α
used␈α
by␈α
present␈α
programs␈α
are␈αoften      ␈↓ π∞␈↓deduction.
␈↓ ↓N␈↓even␈α*weaker␈α)than␈α*the␈α)representations
␈↓ ↓N␈↓themselves.
␈↓ ↓N␈↓α␈↓ ε↑␈↓ `2


␈↓ ↓N␈↓2.␈αDevelopment␈αof␈αtreating␈αconcepts␈αas␈αobjects.   ␈↓ π∞␈↓easy,␈αwhile␈αall␈αthe␈αdi␈↓↓␈↓β@␈↓↓␈↓iculties␈αof␈α
understanding
␈↓ ↓N␈↓This,␈α)described␈α(in␈α)(McCarthy␈α(1977b),            ␈↓ π∞␈↓the␈α∞creative␈α∞processes␈α∞of␈α∞a␈α∞mathematician␈α
are
␈↓ ↓N␈↓facilitates,␈αand␈αmay␈αbe␈αrequired␈αfor,␈αreasoning   ␈↓ π∞␈↓involved␈α∞in␈α∂making␈α∞a␈α∞high␈α∂powered␈α∞theorem
␈↓ ↓N␈↓about␈αknowledge,␈αbelief,␈αwants,␈αpossibility␈αand  ␈↓ π∞␈↓prover.
␈↓ ↓N␈↓necessity.
                                            ␈↓ π∞␈↓However,␈α
in␈α
spite␈αof␈α
the␈α
simplicity␈α
of␈αmodern
␈↓ ↓N␈↓3.␈α≠The␈α≠current␈α~biggest␈α≠gap␈α≠in␈α~computer            ␈↓ π∞␈↓logical␈α→and␈α~set␈α→theoretic␈α→systems␈α~and␈α→the
␈↓ ↓N␈↓reasoning␈α⊗about␈α↔the␈α⊗physical␈α⊗world␈α↔is␈α⊗the         ␈↓ π∞␈↓brevity␈α∂with␈α⊂which␈α∂they␈α⊂permit␈α∂axiomatizing
␈↓ ↓N␈↓complete␈α
lack␈αof␈α
a␈αsystem␈α
for␈α
reasoning␈αabout      ␈↓ π∞␈↓mathematical␈α∩and␈α∩physical␈α∪systems,␈α∩checking
␈↓ ↓N␈↓concurrent␈α
processes.␈α All␈α
the{α
current␈αproblem   ␈↓ π∞␈↓actual␈α≤proofs␈α≤has␈α≤encountered␈α≠fkrmidable
␈↓ ↓N␈↓solving␈α∂programs␈α⊂assume␈α∂that␈α∂each␈α⊂action␈α∂of       ␈↓ π∞␈↓di␈↓↓␈↓β@␈↓↓␈↓iculties.␈α∞ It␈α∞is␈α
easy␈α∞enough␈α∞to␈α∞make␈α
proof-
␈↓ ↓N␈↓the␈α≤program␈α≠produces␈α≤a␈α≠next␈α≤state␈α≠that            ␈↓ π∞␈↓checkers␈α⊂for␈α⊂the␈α⊂formal␈α⊂systems␈α⊂in␈α⊂logic␈α∂and
␈↓ ↓N␈↓depends␈α∂on␈α∂the␈α∂current␈α∂state,␈α∂the␈α∂action,␈α∞and      ␈↓ π∞␈↓set␈α∪theory␈α∪textbooks,␈α∪and␈α∪we␈α∪have␈α∀done␈α∪it.
␈↓ ↓N␈↓sometimes␈α
on␈α
a␈α
random␈α
variable.␈α
 They␈α
don't       ␈↓ π∞␈↓The␈αdi␈↓↓␈↓β@␈↓↓␈↓iculty␈α
is␈αthat␈αthe␈α
formal␈αproofs␈αof␈α
easy
␈↓ ↓N␈↓take␈α∂into␈α∞account␈α∂continuous␈α∞processes␈α∂or␈α∞the     ␈↓ π∞␈↓theorems␈αturn␈α
out␈αto␈αbe␈α
ten␈αtimes␈α
longer␈αthan
␈↓ ↓N␈↓fact␈α∀that␈α∃other␈α∀actions␈α∃and␈α∀events␈α∃may␈α∀be          ␈↓ π∞␈↓informal␈α↔proofs,␈α↔and␈α↔the␈α↔excess␈α↔in␈α↔length
␈↓ ↓N␈↓taking␈α
place.␈α
 We␈α
believe␈α
that␈αcircumscription   ␈↓ π∞␈↓grows␈α→the␈α→further␈α→one␈α→advances␈α→into␈α→the
␈↓ ↓N␈↓may␈α
be␈α
important␈α
in␈α
formalizing␈α
what␈α
people       ␈↓ π∞␈↓theory.␈α∪ The␈α∪trouble␈α∪is␈α∪that␈α∪mathematicians
␈↓ ↓N␈↓know about such processes.                  ␈↓ π∞␈↓have␈α∞not␈α∂succeeded␈α∞in␈α∂completely␈α∞formalizing
                                            ␈↓ π∞␈↓the␈α∀languages␈α∀and␈α∀reasoning␈α∀processes␈α∀they
␈↓ ↓N␈↓4.␈α∂We␈α∂also␈α∂plan␈α∞some␈α∂study␈α∂of␈α∂the␈α∂theory␈α∞of          ␈↓ π∞␈↓actually␈α⊗use.␈α⊗ Much␈α⊗reasoning␈α⊗that␈α⊗at␈α∃␈↓↓␈↓βC␈↓↓␈↓rst
␈↓ ↓N␈↓patterns,␈α∪especially␈α∪higher␈α∪order␈α∀patterns␈α∪in    ␈↓ π∞␈↓seems␈α_to␈α_be␈α↔within␈α_a␈α_given␈α↔mathematical
␈↓ ↓N␈↓which␈αfunction␈αvariables␈αmay␈αbe␈αmatched␈αand       ␈↓ π∞␈↓system,␈αactually␈αis␈αmetamathematical␈αreasoning
␈↓ ↓N␈↓relations␈α∂between␈α∂patterns␈α∞-␈α∂for␈α∂example,␈α∞the     ␈↓ π∞␈↓about␈α1the␈α1system.␈α1 Even␈α2when␈α1a
␈↓ ↓N␈↓relation␈αbetween␈α
a␈αpattern␈α
describing␈αa␈αtype␈α
of    ␈↓ π∞␈↓mathematician␈α
is␈α
working␈α
within␈α
a␈α
system,␈αhe
␈↓ ↓N␈↓three-dimensional␈α
object␈α
such␈α
as␈α
a␈α
person␈αor␈α
a     ␈↓ π∞␈↓establishes␈αshortcuts␈αwhose␈αrepeated␈α
use␈αkeeps
␈↓ ↓N␈↓vehicle␈α∪and␈α∪its␈α∪patterns␈α∪of␈α∪its␈α∀perception␈α∪-       ␈↓ π∞␈↓down the length of a proof.
␈↓ ↓N␈↓such␈α
as␈α∞its␈α
projection␈α
on␈α∞a␈α
retina␈α∞as␈α
modi␈↓↓␈↓βC␈↓↓␈↓ed
␈↓ ↓N␈↓by␈α∂angle␈α∂of␈α∞vision,␈α∂lighting␈α∂and␈α∂occlusion␈α∞by      ␈↓ π∞␈↓We␈αhave␈αa␈α
proof-checker␈αcalled␈αFOL␈α(for␈α
␈↓↓␈↓βC␈↓↓␈↓rst
␈↓ ↓N␈↓other objects.                              ␈↓ π∞␈↓order␈αlogic)␈α(Weyhrauch␈α1977a),␈αwe␈αhave␈α
been
                                            ␈↓ π∞␈↓improving␈α⊃it␈α⊃since␈α⊃1973,␈α⊃and␈α⊃we␈α∩propose␈α⊃to
␈↓ ↓N␈↓In␈α all␈α this␈α∨work,␈α the␈α emphasis␈α is␈α∨on               ␈↓ π∞␈↓improve␈α'it␈α'further␈α'under␈α'this␈α&grant.
␈↓ ↓N␈↓representation␈α≠of␈α≠the␈α≠information␈α≤that␈α≠is        ␈↓ π∞␈↓(Rewriting␈α
it␈α
from␈α∞scratch␈α
will␈α
be␈α∞required␈α
at
␈↓ ↓N␈↓actually␈α⊃available␈α⊂to␈α⊃an␈α⊂observer␈α⊃with␈α⊂given      ␈↓ π∞␈↓some␈α∞point,␈α
but␈α∞we␈α
aren't␈α∞sure␈α
when␈α∞this␈α
will
␈↓ ↓N␈↓opportunities to observe and compute.       ␈↓ π∞␈↓be␈α∂the␈α∂best␈α∂use␈α∂of␈α∂limited␈α⊂manpower).␈α∂ With
                                            ␈↓ π∞␈↓FOL,␈α#we␈α#have␈α#checked␈α#a␈α#variety␈α#of
␈↓ ↓N␈↓α␈↓ α5Proof Checking by Computer                  ␈↓ π∞␈↓mathematical␈α∪proofs,␈α∪and␈α∪each␈α∀such␈α∪project
                                            ␈↓ π∞␈↓has␈α∞told␈α∞us␈α∞something␈α∞about␈α∞how␈α∞to␈α∞improve
␈↓ ↓N␈↓We␈α→must␈α→distinguish␈α→theorem␈α→proving␈α_by           ␈↓ π∞␈↓the␈αproof-checker␈αor␈αhow␈αto␈αformalize␈αa␈αgiven
␈↓ ↓N␈↓computer from proof-checking by computer.   ␈↓ π∞␈↓mathematical␈α∀domain␈α∃or␈α∀how␈α∀to␈α∃write␈α∀and
                                            ␈↓ π∞␈↓debug␈α∀proofs.␈α∃ The␈α∀proofs␈α∃described␈α∀below
␈↓ ↓N␈↓It␈αis␈αan␈α
essential␈αpart␈αof␈α
the␈αnotion␈αof␈αproof␈α
in     ␈↓ π∞␈↓each␈α∪tested␈α∪the␈α∪adaquacy␈α∪of␈α∪FOL␈α∪and␈α∪our
␈↓ ↓N␈↓a␈αformal␈αsystem␈αthat␈αa␈αcandidate␈αproof␈αcan␈αbe       ␈↓ π∞␈↓axiomatizations.
␈↓ ↓N␈↓checked␈α⊗by␈α⊗a␈α↔mechanical␈α⊗process.␈α⊗ It␈α↔is␈α⊗a
␈↓ ↓N␈↓consequence␈α⊃of␈α⊃the␈α⊂work␈α⊃of␈α⊃Goedel,␈α⊂Church         ␈↓ π∞␈↓(a)␈α⊃Any␈α∩device␈α⊃capable␈α⊃of␈α∩accepting␈α⊃general
␈↓ ↓N␈↓and␈α∩Turing␈α⊃that␈α∩no␈α⊃mechanical␈α∩pRocess␈α⊃can         ␈↓ π∞␈↓mathematical␈αreasoning␈αmust␈αbe␈αable␈αto␈αprove
␈↓ ↓N␈↓always␈α∞determine␈α∞whether␈α
a␈α∞proof␈α∞of␈α∞a␈α
given        ␈↓ π∞␈↓theorems␈α⊂of␈α∂arithmetic.␈α⊂ We␈α⊂chose␈α∂"if␈α⊂p␈α⊂is␈α∂a
␈↓ ↓N␈↓sentence␈α≡exists␈α≡in␈α≡a␈α≡formal␈α∨system.␈α≡ In           ␈↓ π∞␈↓prime␈αnumber␈αand␈αp␈αdivides␈αthe␈αproduct␈αa*b,
␈↓ ↓N␈↓principle,␈α∞therefore,␈α
proof-checking␈α∞should␈α
be  ␈↓ π∞␈↓then␈α
p␈α
divides␈α
a␈α
or␈α
p␈α
divides␈α
b."␈α
as␈α
a␈α
typical
                                            ␈↓ π∞␈↓example.
␈↓ ↓N␈↓α␈↓ ε↑␈↓ `3


␈↓ ↓N␈↓(b)␈α∪The␈α∪adequacy␈α∩of␈α∪FOL's␈α∪set␈α∪theory␈α∩was           ␈↓ π∞␈↓encouraging.␈α! These␈α"recent␈α!improvements
␈↓ ↓N␈↓tested␈α∩by␈α∩checking␈α∩both␈α∪Lagrange's␈α∩theorem       ␈↓ π∞␈↓have␈α∞reduced␈α
the␈α∞length␈α
of␈α∞some␈α
proofs␈α∞by␈α
a
␈↓ ↓N␈↓and␈αRamsey's␈αtheorem.␈α These␈αare␈αwell␈αknown       ␈↓ π∞␈↓factor␈α⊂of␈α⊃better␈α⊂than␈α⊃ten.␈α⊂ The␈α⊃reducing␈α⊂the
␈↓ ↓N␈↓theorems␈α0of␈α0mathematics.␈α/ [Lagrange's          ␈↓ π∞␈↓lengths␈α
of␈αproofs␈α
does␈α
not␈αby␈α
itself␈α
mean␈αthat
␈↓ ↓N␈↓theorem:␈α∞the␈α∞order␈α∞of␈α
a␈α∞subgroup␈α∞of␈α∞a␈α
group         ␈↓ π∞␈↓we␈α
are␈α
getting␈α
anywhere.␈α
 Some␈α
of␈α∞the␈α
proofs
␈↓ ↓N␈↓G␈α∞divides␈α∞the␈α∂order␈α∞of␈α∞G;␈α∂Ramsey's␈α∞theorem:        ␈↓ π∞␈↓we␈α⊂are␈α⊂now␈α⊃producing␈α⊂are␈α⊂about␈α⊂as␈α⊃long␈α⊂as
␈↓ ↓N␈↓let␈αG␈α
be␈αa␈α
countably␈αin␈↓↓␈↓βC␈↓↓␈↓nite␈α
set␈αof␈αpoints,␈α
each     ␈↓ π∞␈↓their␈α⊂informal␈α∂versions.␈α⊂ This␈α∂is␈α⊂most␈α∂clearly
␈↓ ↓N␈↓point␈α∀being␈α∀connected␈α∀to␈α∀every␈α∀other␈α∀by␈α∪a          ␈↓ π∞␈↓evident␈α_in␈α_the␈α_␈↓↓samefringe␈↓␈α→example␈α_below.
␈↓ ↓N␈↓thread,␈αeach␈αthread␈αbeing␈αred␈αor␈αblack.␈α Then      ␈↓ π∞␈↓Here are three of our recent experiments:
␈↓ ↓N␈↓there␈αis␈αan␈α
in␈↓↓␈↓βC␈↓↓␈↓nite␈αsubset␈αof␈αthese␈α
points␈αsuch
␈↓ ↓N␈↓that␈α∞the␈α∞connecting␈α∞threads␈α∞within␈α∂the␈α∞subset     ␈↓ π∞␈↓Filman[..]␈α∀has␈α∀used␈α∀FOL␈α∀to␈α∀show␈α∀that␈α∪the
␈↓ ↓N␈↓are all of the same color.]                 ␈↓ π∞␈↓reasoning␈α∞involved␈α∂in␈α∞the␈α∂solution␈α∞of␈α∂a␈α∞hard
                                            ␈↓ π∞␈↓retrospective␈α
chess␈α
problem␈α
can␈α
be␈αformalized
␈↓ ↓N␈↓(c)␈α∞Wilson's␈α∞theorem␈α∞that␈α∞"If␈α∞p␈α∞is␈α∂prime␈α∞then       ␈↓ π∞␈↓in␈α∩␈↓↓␈↓βC␈↓↓␈↓rst␈α∩order␈α⊃logic.␈α∩ We␈α∩chose␈α∩this␈α⊃example
␈↓ ↓N␈↓(p-1)!␈αhas␈αthe␈αremainder␈αp-1␈αwhen␈αdivided␈αby       ␈↓ π∞␈↓from␈α→outside␈α→mathematics,␈α~because␈α→human
␈↓ ↓N␈↓p"␈α∪is␈α∀a␈α∪purely␈α∀arithmetic␈α∪statement,␈α∀but␈α∪its       ␈↓ π∞␈↓reasoning␈α)often␈α(mixes␈α)deduction␈α(with
␈↓ ↓N␈↓proof␈α∂uses␈α⊂a␈α∂pairing␈α∂argument␈α⊂(requiring␈α∂set      ␈↓ π∞␈↓observation␈α#of␈α"the␈α#outside␈α#world,␈α"and
␈↓ ↓N␈↓theory)␈α↔which␈α↔is␈α⊗beyond␈α↔the␈α↔capability␈α⊗of         ␈↓ π∞␈↓observation␈α_of␈α_a␈α_chess␈α_␈↓↓partial␈α→position␈↓␈α_is
␈↓ ↓N␈↓present theorem-proving programs.           ␈↓ π∞␈↓prominent␈α↔in␈α↔this␈α↔example.␈α↔ The␈α↔semantic
                                            ␈↓ π∞␈↓attachment␈α∩mechanism␈α⊃of␈α∩FOL␈α⊃was␈α∩used␈α⊃to
␈↓ ↓N␈↓(d)␈α
We␈α
checked␈α
the␈α
␈↓↓␈↓βC␈↓↓␈↓rst␈α
one␈α
hundred␈α
theorems       ␈↓ π∞␈↓build␈α∪a␈α∪simulation␈α∀of␈α∪his␈α∪chess␈α∀world.␈α∪ He
␈↓ ↓N␈↓of␈α⊗set␈α∃theory␈α⊗as␈α∃presented␈α⊗in␈α∃KELLEY[..].         ␈↓ π∞␈↓could␈α_then␈α_use␈α_the␈α→semantic␈α_simpli␈↓↓␈↓βC␈↓↓␈↓cation
␈↓ ↓N␈↓This␈α∩was␈α∩for␈α∩the␈α∩purpose␈α∩of␈α∪establishing␈α∩a         ␈↓ π∞␈↓routines␈α∂of␈α∂FOL␈α∂to␈α∂answer␈α∂(in␈α∂a␈α∂single␈α∂step)
␈↓ ↓N␈↓large␈α~collection␈α~of␈α~proofs␈α~to␈α~be␈α~used␈α~as           ␈↓ π∞␈↓questions␈α⊂like␈α⊂"is␈α⊂he␈α⊂black␈α⊂king␈α⊂in␈α⊂check␈α∂on
␈↓ ↓N␈↓benchmarks to measure later ideas.          ␈↓ π∞␈↓board␈αB"␈αby␈αlooking␈αat␈αhis␈αmodel,␈αrather␈αthan
                                            ␈↓ π∞␈↓deducing␈α
from␈αaxioms␈α
about␈αthe␈α
rules␈αof␈α
chess
␈↓ ↓N␈↓(e)␈α⊂The␈α⊂problem␈α⊂of␈α⊂formalizing␈α⊂how␈α⊂we␈α∂can          ␈↓ π∞␈↓that␈α⊂black␈α⊂was␈α⊂in␈α⊂check.␈α⊂ This␈α⊂single␈α⊂use␈α⊂of
␈↓ ↓N␈↓reason␈α∃about␈α∀what␈α∃other␈α∀people␈α∃know␈α∀was           ␈↓ π∞␈↓semantic␈α∪attachment␈α∪saves␈α∀several␈α∪hundered
␈↓ ↓N␈↓illustrated␈α~by␈α≠axiomatizing␈α~the␈α≠wise␈α~man         ␈↓ π∞␈↓steps␈αover␈αtraditional␈αformalizations.␈α Filman's
␈↓ ↓N␈↓problem[Mc&Sato].␈α) One␈α)of␈α)the␈α)hard              ␈↓ π∞␈↓proof␈α⊂is␈α⊂still␈α⊂much␈α⊂longer␈α⊂than␈α⊂the␈α⊂informal
␈↓ ↓N␈↓problems␈α∀here␈α∪was␈α∀to␈α∪formulate␈α∀and␈α∪prove          ␈↓ π∞␈↓proof,␈α≥showing␈α≥that␈α≥we␈α≥still␈α≥don't␈α≥fully
␈↓ ↓N␈↓that␈α∞some␈α∞else␈α∞doesn't␈α∞know␈α∞something.␈α∞ This      ␈↓ π∞␈↓understand␈α
how␈αhumans␈α
combine␈αobservation
␈↓ ↓N␈↓problem␈α∂was␈α∂also␈α∂axiomatized␈α∂in␈α∂second␈α∞way        ␈↓ π∞␈↓with deduction.
␈↓ ↓N␈↓by Chris Goad.
                                            ␈↓ π∞␈↓We␈α∂have␈α∂preliminary␈α∂estimates␈α∂of␈α⊂the␈α∂length
␈↓ ↓N␈↓(f)␈α"We␈α!proved␈α"the␈α!correctness␈α"of␈α!the              ␈↓ π∞␈↓of␈α⊗the␈α⊗Kelley␈α⊗set␈α⊗theory␈α⊗proofs␈α⊗mentioned
␈↓ ↓N␈↓McCarthy-Painter␈α?␈α∂compiler[Mc&painter].       ␈↓ π∞␈↓above.␈α∪ In␈α∪an␈α∩initial␈α∪experiment␈α∪using␈α∩only
␈↓ ↓N␈↓This␈α∂allowed␈α∂us␈α∞to␈α∂compare␈α∂the␈α∂original␈α∞␈↓↓␈↓βC␈↓↓␈↓rst       ␈↓ π∞␈↓part␈α∀of␈α∪the␈α∀currently␈α∪available␈α∀features,␈α∪we
␈↓ ↓N␈↓order␈α*proof␈α*with␈α*some␈α*more␈α)recent                ␈↓ π∞␈↓reduced␈α↔the␈α↔number␈α↔of␈α↔steps␈α↔necessary␈α↔to
␈↓ ↓N␈↓proofs[rww&rgm,boyer&moore]                 ␈↓ π∞␈↓prove␈α
the␈α
␈↓↓␈↓βC␈↓↓␈↓rst␈αthirty␈α
three␈α
theorems␈α
from␈α461
                                            ␈↓ π∞␈↓to␈α104.␈α Considering␈αthat␈αit␈αtakes␈αone␈αstep␈αjust
␈↓ ↓N␈↓Recent␈αimprovements␈αhave␈αreduced␈αthe␈αlength      ␈↓ π∞␈↓to␈α#express␈α#the␈α"theorem,␈α#this␈α#is␈α"quite
␈↓ ↓N␈↓of␈α
some␈α
proofs␈α
by␈αa␈α
factor␈α
of␈α
better␈α
than␈αten.       ␈↓ π∞␈↓impressive.␈α∞ We␈α∞expect␈α∞that␈α∞adding␈α∞the␈α
goal-
␈↓ ↓N␈↓Here␈α∂are␈α⊂some␈α∂of␈α∂them␈α⊂and␈α∂what␈α⊂they␈α∂have            ␈↓ π∞␈↓structure␈α#features␈α#mentioned␈α$below␈α#will
␈↓ ↓N␈↓accomplished.                               ␈↓ π∞␈↓substantially reduce these proof lengths.

␈↓ ↓N␈↓After␈αa␈α
period␈αof␈αadding␈α
new␈αfeatures␈αto␈α
FOL        ␈↓ π∞␈↓In␈α⊃connection␈α⊃with␈α⊃McCarthy's␈α⊃recent␈α⊃(1977)
␈↓ ↓N␈↓we␈α↔have␈α↔again␈α⊗begun␈α↔to␈α↔experiment␈α⊗with            ␈↓ π∞␈↓formalization␈α&of␈α&LISP␈α&programs␈α&using
␈↓ ↓N␈↓proofs␈α)and␈α*our␈α)initial␈α*successes␈α)are             ␈↓ π∞␈↓sentences␈αand␈αschemata␈αof␈α␈↓↓␈↓βC␈↓↓␈↓rst␈αorder␈α
logic,␈αwe
␈↓ ↓N␈↓α␈↓ ε↑␈↓ ]4


␈↓ ↓N␈↓have␈α
checked␈α
a␈α
FOL␈α
proof␈α
of␈α∞the␈α
correctness        ␈↓ π∞␈↓the␈α∪work␈α∪of␈α∪Wagner[..].␈α∪ Almost␈α∪all␈α∩present
␈↓ ↓N␈↓of␈αhis␈α␈↓↓samefringe␈↓␈αprogram.␈α ␈↓↓samefringe[x,y]␈↓␈α
is   ␈↓ π∞␈↓hardware␈αveri␈↓↓␈↓βC␈↓↓␈↓cation␈αis␈αbased␈αon␈αsimulating␈α
it
␈↓ ↓N␈↓turns␈α∀true␈α∀if␈α∀the␈α∀S-expressions␈α∀⊗x␈α∀and␈α∀⊗y          ␈↓ π∞␈↓in␈α∀all␈α∃posible␈α∀states.␈α∃ Wagner␈α∀demonstrated
␈↓ ↓N␈↓have␈αthe␈αsame␈αatoms␈αin␈αthe␈αsame␈αorder.␈α This        ␈↓ π∞␈↓that␈α
formal␈α
proofs␈αthat␈α
the␈α
hardware␈αis␈α
correct
␈↓ ↓N␈↓proof␈α∩as␈α⊃checked␈α∩by␈α⊃FOL␈α∩was␈α⊃of␈α∩the␈α⊃same             ␈↓ π∞␈↓are␈α_feasible␈α→and␈α_require␈α_less␈α→human␈α_and
␈↓ ↓N␈↓length␈α∞as␈α
a␈α∞written␈α∞out␈α
informal␈α∞proof␈α∞of␈α
the       ␈↓ π∞␈↓compter␈α
work␈α∞than␈α
the␈α∞simulation␈α
techniques.
␈↓ ↓N␈↓same␈α⊂result.␈α∂ We␈α⊂believe␈α∂that␈α⊂such␈α∂favorable      ␈↓ π∞␈↓We propose to continue this work.
␈↓ ↓N␈↓results are generally possible.
                                            ␈↓ π∞␈↓(4)␈α
We␈α
intend␈α∞to␈α
redo␈α
the␈α
theorems␈α∞of␈α
Kelley
␈↓ ↓N␈↓Our plans for FOL include the following:    ␈↓ π∞␈↓mentioned␈αabove␈αusing␈αthe␈αmany␈αnew␈αfeatures
                                            ␈↓ π∞␈↓that␈αhave␈αbeen␈αadded␈αto␈αFOL.␈α These␈αinclude
␈↓ ↓N␈↓(1)␈αThe␈αveri␈↓↓␈↓βC␈↓↓␈↓cation␈αof␈αthe␈αcorrectness␈αof␈αLISP     ␈↓ π∞␈↓the␈αsyntatic␈αsimpli␈↓↓␈↓βC␈↓↓␈↓er,␈αthe␈αsemantic␈αattachment
␈↓ ↓N␈↓programs.␈α→ John␈α→McCarthy[..]␈α~has␈α→recently       ␈↓ π∞␈↓mechanism, and various decision proceedures.
␈↓ ↓N␈↓begun␈α↔using␈α↔axiom␈α↔schemas␈α↔to␈α↔prove␈α↔the
␈↓ ↓N␈↓properties␈α⊃of␈α⊂LISP␈α⊃programs.␈α⊂ We␈α⊃intend␈α⊂to        ␈↓ π∞␈↓(5)␈α≥Introduce␈α≥metamathematical␈α≤machinery
␈↓ ↓N␈↓expand␈α≥this␈α≥work␈α≥by␈α≡introducing␈α≥meta-            ␈↓ π∞␈↓into␈αFOL.␈α This␈αwill␈αallow␈αus␈αto␈αbegin␈αto␈αstate
␈↓ ↓N␈↓mathematical␈αmachinery␈αinto␈αFOL␈α(see␈α
below).     ␈↓ π∞␈↓and␈α≡prove␈α≥theorems␈α≡about␈α≥how␈α≡we␈α≥do
␈↓ ↓N␈↓This␈αwill␈αbe␈αfollowed␈αby␈αa␈αmajor␈αe␈↓↓␈↓β@␈↓↓␈↓ort␈αto␈αuse        ␈↓ π∞␈↓reasoning␈α∩in␈α∩the␈α∩logic.␈α∩ The␈α∩implications␈α∩of
␈↓ ↓N␈↓McCarthy's␈α∀axiomatization␈α∃of␈α∀LISP␈α∃and␈α∀to         ␈↓ π∞␈↓this␈α
are␈α
very␈α∞broad.␈α
 As␈α
mentioned␈α∞above␈α
we
␈↓ ↓N␈↓prove␈α∃properties␈α∀of␈α∃simple␈α∃LISP␈α∀programs.        ␈↓ π∞␈↓will␈α↔be␈α↔able␈α↔to␈α↔state,␈α↔as␈α↔sentences␈α↔of␈α↔the
␈↓ ↓N␈↓Weyhrauch␈α
has␈α∞recently␈α
pointed␈α
out␈α∞that␈α
this      ␈↓ π∞␈↓metamathematics,␈α_axiom␈α_schemas␈α_useful␈α↔in
␈↓ ↓N␈↓same␈αtechnique␈α
can␈αbe␈α
used␈αto␈α
formulate␈αpart       ␈↓ π∞␈↓proving␈α⊗the␈α∃correctness␈α⊗of␈α⊗LISP␈α∃programs.
␈↓ ↓N␈↓of␈α∀Dana␈α∃Scott's␈α∀computation␈α∃induction␈α∀into       ␈↓ π∞␈↓Another␈α%application␈α$of␈α%schemas␈α%is␈α$to
␈↓ ↓N␈↓␈↓↓␈↓βC␈↓↓␈↓rst␈α≠order␈α≠logic.␈α≠ This␈α≠also␈α≤requires␈α≠the         ␈↓ π∞␈↓axiomatizing circumscription.
␈↓ ↓N␈↓metamathematical␈α∞machinery.␈α
 We␈α∞expect␈α
this
␈↓ ↓N␈↓to␈α⊂be␈α⊂su␈↓↓␈↓β@␈↓↓␈↓iciently␈α⊃practical␈α⊂for␈α⊂us␈α⊂to␈α⊃use␈α⊂this      ␈↓ π∞␈↓(6)␈α
The␈α
usefulness␈α
of␈α
the␈α
metamathematics␈α
will
␈↓ ↓N␈↓axiomatization in Stanford LISP courses.    ␈↓ π∞␈↓be␈α≠enhanced␈α≠by␈α~our␈α≠addition␈α≠of␈α~certain
                                            ␈↓ π∞␈↓re␈↓↓␈↓βD␈↓↓␈↓ection␈αprinciples.␈α These␈αare␈αrules␈αthat␈α
state
␈↓ ↓N␈↓(2)␈αAnother␈αaspect␈αof␈αprogram␈αveri␈↓↓␈↓βC␈↓↓␈↓cation␈αare     ␈↓ π∞␈↓some␈α≤relation␈α≥between␈α≤a␈α≤theory␈α≥and␈α≤its
␈↓ ↓N␈↓what␈α≤are␈α≠called␈α≤intensional␈α≤properties␈α≠of        ␈↓ π∞␈↓metamathematics.␈α⊃ For␈α⊃example,␈α⊃if␈α⊃you␈α⊃have
␈↓ ↓N␈↓programs.␈α_ These␈α_include␈α_things␈α→like␈α_how         ␈↓ π∞␈↓proved␈α⊂a␈α∂certain␈α⊂formula,␈α∂then␈α⊂in␈α⊂the␈α∂meta-
␈↓ ↓N␈↓much␈α
storage␈α
a␈α
program␈α
uses,␈α
and␈α
how␈α
many          ␈↓ π∞␈↓theory␈α⊗you␈α⊗can␈α⊗assert␈α⊗that␈α⊗the␈α⊗formula␈α∃is
␈↓ ↓N␈↓steps␈α↔it␈α↔takes.␈α↔ These␈α↔questions␈α↔cannot␈α⊗be        ␈↓ π∞␈↓provable.␈α∀ Conversely,␈α∀informal␈α∀mathematics
␈↓ ↓N␈↓asked␈α
by␈α
current␈α
formalisms␈α
for␈αmathematical     ␈↓ π∞␈↓often␈αuses␈αmetamathematical␈αassertions␈αthat␈α
all
␈↓ ↓N␈↓theory␈α⊂of␈α⊂computation.␈α⊂ The␈α⊂require␈α∂theories     ␈↓ π∞␈↓formulas␈α
with␈αcertain␈α
properties␈α
are␈αtrue.␈α
 The
␈↓ ↓N␈↓that␈αcontain␈α
programs␈αas␈α
objects␈αand␈α
can␈αtalk      ␈↓ π∞␈↓attachment␈α0mechanism␈α0combined␈α/with
␈↓ ↓N␈↓about␈α∞the␈α∞abstract␈α
properties␈α∞of␈α∞the␈α
machines     ␈↓ π∞␈↓re␈↓↓␈↓βD␈↓↓␈↓ection␈α)principles␈α(will␈α)allow␈α)us␈α(to
␈↓ ↓N␈↓that␈α
they␈α
run␈α
on.␈α
 Most␈α
previous␈αformal␈α
e␈↓↓␈↓β@␈↓↓␈↓orts     ␈↓ π∞␈↓automatically␈α
use␈α
such␈α
metatheorems␈α
to␈α
prove
␈↓ ↓N␈↓have␈α
only␈α
shown␈α
properties␈α
of␈α∞the␈α
algorithms      ␈↓ π∞␈↓theorems in the base theory.
␈↓ ↓N␈↓computed␈α~by␈α~programs,␈α~not␈α≠properties␈α~of
␈↓ ↓N␈↓programs␈α∞themselves.␈α∞ One␈α∞exception␈α∞was␈α
the      ␈↓ π∞␈↓α␈↓ λ⎇Personnel 
␈↓ ↓N␈↓work␈α∃of␈α∀Aiello,␈α∃L.,␈α∀Aiello,␈α∃M.,␈α∀Weyhrauch,
␈↓ ↓N␈↓R[..],␈α⊗on␈α↔PASCAL.␈α⊗ This␈α⊗was␈α↔carried␈α⊗out           ␈↓ π∞␈↓Richard␈αWeyhrauch␈αis␈αthe␈αmain␈αdesigner␈αand
␈↓ ↓N␈↓using␈αanother␈αformal␈αsystem␈αand␈αwe␈αhave␈αjust       ␈↓ π∞␈↓implementer␈α∀of␈α∀FOL.␈α∀ This␈α∀requires␈α∀a␈α∪full
␈↓ ↓N␈↓begun␈α
to␈α
think␈αabout␈α
such␈α
problems␈αusing␈α
␈↓↓␈↓βC␈↓↓␈↓rst      ␈↓ π∞␈↓understanding␈α⊃of␈α⊃both␈α⊃modern␈α⊃mathematical
␈↓ ↓N␈↓order logic.                                ␈↓ π∞␈↓logic,␈αprogramming␈α
techniques␈αand␈α
the␈αability
                                            ␈↓ π∞␈↓to do good human engineering.
␈↓ ↓N␈↓(3)␈α→The␈α→veri␈↓↓␈↓βC␈↓↓␈↓cation␈α→of␈α→the␈α→correctness␈α_of
␈↓ ↓N␈↓hardware␈αcircuit␈α
design␈αusing␈αFOL␈α
continuing     ␈↓ π∞␈↓The␈αFOL␈αproject␈αattracts␈αconsiderable␈αinterest
␈↓ ↓N␈↓α␈↓ ε↑␈↓ ←5


␈↓ ↓N␈↓from␈α⊃young␈α⊃mathematicians␈α⊃who␈α⊃would␈α⊂like,        ␈↓ π∞␈↓Organized and directs Stanford Arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓N␈↓␈↓↓␈↓βC␈↓↓␈↓nally,␈α+to␈α+see␈α+computers␈α+applied␈α*to              ␈↓ π∞␈↓␈↓ πNIntelligence Project
␈↓ ↓N␈↓mathematical␈αresearch␈αin␈αa␈αsigni␈↓↓␈↓βC␈↓↓␈↓cant␈αway.␈α A     ␈↓ π∞␈↓Developed the LISP programming system for
␈↓ ↓N␈↓rotating␈α≠research␈α~associateship␈α≠will␈α~bene␈↓↓␈↓βC␈↓↓␈↓t     ␈↓ π∞␈↓␈↓ πNcomputing with symbolic expressions,
␈↓ ↓N␈↓both␈α(proof-checking␈α'research␈α(and␈α'the            ␈↓ π∞␈↓␈↓ πNparticipated in the development of the
␈↓ ↓N␈↓propagation of its results.                 ␈↓ π∞␈↓␈↓ πNALGOL 58 and the ALGOL 60
                                            ␈↓ π∞␈↓␈↓ πNlanguages.
␈↓ ↓N␈↓α␈↓ α7Biography of John McCarthy                  ␈↓ π∞␈↓Present scienti␈↓↓␈↓βC␈↓↓␈↓c work is in the ␈↓↓␈↓βC␈↓↓␈↓elds of
                                            ␈↓ π∞␈↓␈↓ πNArti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence, Computation with
␈↓ ↓N␈↓BORN: September 4, 1927 in Boston,          ␈↓ π∞␈↓␈↓ πNSymbolic Expressions, Mathematical
␈↓ ↓N␈↓␈↓ α∞Massachusetts                               ␈↓ π∞␈↓␈↓ πNTheory of Computation, Time-Sharing
                                            ␈↓ π∞␈↓␈↓ πNcomputer systems.
␈↓ ↓N␈↓EDUCATION:                                  ␈↓ π∞␈↓PUBLICATIONS:
␈↓ ↓N␈↓B.S.  (Mathematics) California Institute of ␈↓ π∞␈↓[1] "Towards a Mathematical Theory of
␈↓ ↓N␈↓␈↓ α∞Technology, 1948.                           ␈↓ π∞␈↓␈↓ πNComputation", in ␈↓↓Proc. IFIP Congress
␈↓ ↓N␈↓Ph.D. (Mathematics) Princeton University,   ␈↓ π∞␈↓↓␈↓ πN62␈↓, North-Holland, Amsterdam, 1963.
␈↓ ↓N␈↓␈↓ α∞1951.                                       ␈↓ π∞␈↓[2] "A Basis for a Mathematical Theory of
                                            ␈↓ π∞␈↓␈↓ πNComputation", in P. Bia␈↓↓␈↓β@␈↓↓␈↓ort and D.
␈↓ ↓N␈↓HONORS AND SOCIETIES:                       ␈↓ π∞␈↓␈↓ πNHershberg (eds.), ␈↓↓Computer Programming
␈↓ ↓N␈↓American Mathematical Society,              ␈↓ π∞␈↓↓␈↓ πNand Formal Systems␈↓, North-Holland,
␈↓ ↓N␈↓Association for Computing Machinery,        ␈↓ π∞␈↓␈↓ πNAmsterdam, 1963.
␈↓ ↓N␈↓Sigma Xi,                                   ␈↓ π∞␈↓[3] (with S. Boilen, E. Fredkin, J.C.R.
␈↓ ↓N␈↓Sloan Fellow in Physical Science (1957-59), ␈↓ π∞␈↓␈↓ πNLicklider) "A Time-Sharing Debugging
␈↓ ↓N␈↓ACM National Lecturer (1961),               ␈↓ π∞␈↓␈↓ πNSystem for a Small Computer", ␈↓↓Proc.
␈↓ ↓N␈↓IEEE,                                       ␈↓ π∞␈↓↓␈↓ πNAFIPS Conf.␈↓ (SJCC), Vol. 23, 1963.
␈↓ ↓N␈↓A.M. Turing Award from Association for      ␈↓ π∞␈↓[4] (with F. Corbato, M. Daggett) "The
␈↓ ↓N␈↓␈↓ α∞Computing Machinery (1971).                 ␈↓ π∞␈↓␈↓ πNLinking Segment Subprogram Language
                                            ␈↓ π∞␈↓␈↓ πNand Linking Loader Programming
␈↓ ↓N␈↓PROFESSIONAL EXPERIENCE:                    ␈↓ π∞␈↓␈↓ πNLanguages", ␈↓↓Comm. ACM␈↓, July 1963.
␈↓ ↓N␈↓Proctor Fellow, Princeton University (1950- ␈↓ π∞␈↓[5] "Problems in the Theory of Computation",
␈↓ ↓N␈↓␈↓ α∞51),                                        ␈↓ π∞␈↓␈↓ πN␈↓↓Proc. IFIP Congress 1965␈↓.
␈↓ ↓N␈↓Higgins Research Instructor in Mathematics, ␈↓ π∞␈↓[6] "Time-Sharing Computer Systems", in W.
␈↓ ↓N␈↓␈↓ α∞Princeton University (1951-53),             ␈↓ π∞␈↓␈↓ πNOrr (ed.), ␈↓↓Conversational Computers␈↓,
␈↓ ↓N␈↓Acting Assistant Professor of Mathematics,  ␈↓ π∞␈↓␈↓ πNWiley, 1966.
␈↓ ↓N␈↓␈↓ α∞Stanford University (1953-55),              ␈↓ π∞␈↓[7] "A Formal Description of a Subset of
␈↓ ↓N␈↓Assistant Professor of Mathematics,         ␈↓ π∞␈↓␈↓ πNAlgol", in T.  Steele (ed.), ␈↓↓Formal
␈↓ ↓N␈↓␈↓ α∞Dartmouth College (1955-58),                ␈↓ π∞␈↓↓␈↓ πNLanguage Description Languages for
␈↓ ↓N␈↓Assistant Professor of Communication Science,␈↓ π∞␈↓↓␈↓ πNComputer Programming␈↓, North-Holland,
␈↓ ↓N␈↓␈↓ α∞M.I.T. (1958-61),                           ␈↓ π∞␈↓␈↓ πNAmsterdam, 1966.
␈↓ ↓N␈↓Associate Professor of Communication        ␈↓ π∞␈↓[8] "Information", ␈↓↓Scienti␈↓␈↓βS␈↓␈↓↓c American␈↓,
␈↓ ↓N␈↓␈↓ α∞Science, M.I.T. (1961-62),                  ␈↓ π∞␈↓␈↓ πNSeptember 1966.
␈↓ ↓N␈↓Professor of Computer Science Stanford      ␈↓ π∞␈↓[9] "Computer Control of a Hand and Eye", in
␈↓ ↓N␈↓␈↓ α∞University (1962 - present).                ␈↓ π∞␈↓␈↓ πN␈↓↓Proc.  Third All-Union Conference on
                                            ␈↓ π∞␈↓↓␈↓ πNAutomatic Control (Technical Cybernetics)␈↓,
␈↓ ↓N␈↓PROFESSIONAL RESPONSIBILITIES               ␈↓ π∞␈↓␈↓ πNNauka, Moscow, 1967 (Russian).
␈↓ ↓N␈↓␈↓ α∞AND SCIENTIFIC INTERESTS:                   ␈↓ π∞␈↓[10] (with D. Brian, G. Feldman, and J. Allen)
␈↓ ↓N␈↓With Marvin Minsky organized and directed   ␈↓ π∞␈↓␈↓ πN"THOR ␈↓↓␈↓βE␈↓↓␈↓ A Display Based Time-
␈↓ ↓N␈↓␈↓ α∞the Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence Project at       ␈↓ π∞␈↓␈↓ πNSharing System", ␈↓↓Proc. AFIPS Conf.␈↓
␈↓ ↓N␈↓␈↓ α∞M.I.T.                                      ␈↓ π∞␈↓␈↓ πN(FJCC), Vol.  30, Thompson,
                                            ␈↓ π∞␈↓␈↓ πNWashington, D.C., 1967.
␈↓ ↓N␈↓α␈↓ ε↑␈↓ ←6


␈↓ ↓N␈↓[11] (with James Painter) "Correctness of a
␈↓ ↓N␈↓␈↓ α∞Compiler for Arithmetic Expressions",
␈↓ ↓N␈↓␈↓ α∞Amer. Math. Soc., ␈↓↓Proc. Symposia in
␈↓ ↓N␈↓↓␈↓ α∞Applied Math., Math. Aspects of
␈↓ ↓N␈↓↓␈↓ α∞Computer Science␈↓, New York, 1967.
␈↓ ↓N␈↓[12] "Programs with Common Sense", in
␈↓ ↓N␈↓␈↓ α∞Marvin Minsky (ed.), ␈↓↓Semantic
␈↓ ↓N␈↓↓␈↓ α∞Information Processing␈↓, MIT Press,
␈↓ ↓N␈↓␈↓ α∞Cambridge, 1968.
␈↓ ↓N␈↓[13] (with Lester Earnest, D. Raj. Reddy,
␈↓ ↓N␈↓␈↓ α∞Pierre Vicens) "A Computer with Hands,
␈↓ ↓N␈↓␈↓ α∞Eyes, and Ears", ␈↓↓Proc. AFIPS Conf.␈↓
␈↓ ↓N␈↓␈↓ α∞(FJCC), 1968.
␈↓ ↓N␈↓[14] (with Patrick Hayes) "Some Philosophical
␈↓ ↓N␈↓␈↓ α∞Problems from the Standpoint of
␈↓ ↓N␈↓␈↓ α∞Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence", in Donald Michie
␈↓ ↓N␈↓␈↓ α∞(ed.), ␈↓↓Machine Intelligence 4␈↓, American
␈↓ ↓N␈↓␈↓ α∞Elsevier, New York, 1969.
␈↓ ↓N␈↓[15] "The Home Information Terminal", ␈↓↓Man
␈↓ ↓N␈↓↓␈↓ α∞and Computer, Proc. Int. Conf., Bordeaux,
␈↓ ↓N␈↓↓␈↓ α∞1970␈↓, S. Karger, New York, 1972.
␈↓ ↓N␈↓α␈↓ ε↑␈↓ `7


␈↓ ↓N␈↓α␈↓ ε/Budget 

␈↓ ↓N␈↓∧PERIOD COVERED: 3 Years: 1 Jan. 1978 through 31 December 1980.

␈↓ ↓N␈↓∧Dates:                1/1/78-12/31/78   1/1/79-12/31/79   1/1/80-12/31/80

␈↓ ↓N␈↓∧A. SALARIES AND WAGES

␈↓ ↓N␈↓∧   1.Senior Personnel:

␈↓ ↓N␈↓∧     a.John McCarthy,      7,575.            8,181.           8,835.
␈↓ ↓N␈↓∧       Professor
␈↓ ↓N␈↓∧       Summer 75%
␈↓ ↓N␈↓∧       Acad. Yr. 0%

␈↓ ↓N␈↓∧   2.Other Personnel

␈↓ ↓N␈↓∧     a.Research Associates

␈↓ ↓N␈↓∧       (1)R.Weyhrauch     10,400.           11,232.          12,131.
␈↓ ↓N␈↓∧          50% - 12 months
␈↓ ↓N␈↓∧                                
␈↓ ↓N␈↓∧       (2) ________,      17,000.           18,360.          19,829.
␈↓ ↓N␈↓∧          100% - 12 months

␈↓ ↓N␈↓∧     b. Student Research 
␈↓ ↓N␈↓∧        Assistants
␈↓ ↓N␈↓∧        (50% Acad.Yr.;
␈↓ ↓N␈↓∧        100% Summer)

␈↓ ↓N␈↓∧       (1)                 7,155.            7,704.           8,320.

␈↓ ↓N␈↓∧       (2)                 7,155.            7,704.           8,320.

␈↓ ↓N␈↓∧     c. Support Personnel

␈↓ ↓N␈↓∧       (1)Secty(25%)       2,615.            2,824.           3,050.
␈↓ ↓N␈↓∧    
␈↓ ↓N␈↓∧       (2)Elec.Tech.(25%)  4,895.            5,287.           5,710.
␈↓ ↓N␈↓∧                          _______           _______          _______

␈↓ ↓N␈↓∧   Total Salaries & Wages 56,795.           61,292.          66,195.

␈↓ ↓N␈↓∧B. STAFF BENEFITS         
␈↓ ↓N␈↓∧   9/1/77-8/31/78:20.0%          
␈↓ ↓N␈↓∧   9/1/78-8/31/79:20.8%
␈↓ ↓N␈↓∧   9/1/79-8/31/80;21.6%                                          
␈↓ ↓N␈↓∧   9/1/80-8/31/81;22.4%
␈↓ ↓N␈↓∧                          11,510.           12,912.          14,475.
␈↓ ↓N␈↓∧                          _______          ________         ________
␈↓ ↓N␈↓∧C. TOTAL SALARIES, WAGES,
␈↓ ↓N␈↓∧   AND STAFF BENEFITS     68,305.           74,204.          80,670.
␈↓ ↓N␈↓α␈↓ ε↑␈↓ ←8


␈↓ ↓N␈↓∧D. PERMANENT EQUIPMENT        --                --               --

␈↓ ↓N␈↓∧E. EXPENDABLE SUPPLIES     2,040.            2,040.           2,040.
␈↓ ↓N␈↓∧   & EQUIPMENT(e.g.,copying,
␈↓ ↓N␈↓∧   office supplies, postage,      
␈↓ ↓N␈↓∧   freight, consulting,
␈↓ ↓N␈↓∧   honoraria)

␈↓ ↓N␈↓∧F. TRAVEL                  2,300.            2,300.           2,300.
␈↓ ↓N␈↓∧   All Domestic Travel

␈↓ ↓N␈↓∧G. PUBLICATIONS            1,200.            1,200.           1,200.

␈↓ ↓N␈↓∧H. OTHER COSTS             8,300.            8,300.           8,300.
␈↓ ↓N␈↓∧   1.Communication  2,000.
␈↓ ↓N␈↓∧     (telephone)     
␈↓ ↓N␈↓∧   2. Computer      6,300.
␈↓ ↓N␈↓∧      Equip. Maint.
␈↓ ↓N␈↓∧                          _______          ________          _______  

␈↓ ↓N␈↓∧I. TOTAL COSTS             82,145.          88,044.          94,510.
␈↓ ↓N␈↓∧    (A through H)

␈↓ ↓N␈↓∧J. INDIRECT COSTS:58% of   47,644.          51,066.          54,816.
␈↓ ↓N␈↓∧   A through H, less D.   ________         ________         ________     


␈↓ ↓N␈↓∧K. TOTAL COSTS            129,789.         139,110.         149,326.
␈↓ ↓N␈↓α␈↓ ε↑␈↓ `9


␈↓ ↓N␈↓α␈↓ β5References                                  ␈↓ π∞␈↓Notes for NSF proposal

␈↓ ↓N␈↓␈↓αMcCarthy, J. and Hayes, P.J.␈↓ (1969) Some    ␈↓ π∞␈↓What:␈α∪Proof␈α∪checking,␈α∪epistemology,␈α∪general
␈↓ ↓N␈↓␈↓ ↓}Philosophical Problems from the             ␈↓ π∞␈↓basic research.
␈↓ ↓N␈↓␈↓ ↓}Standpoint of Arti␈↓α␈↓βC␈↓α␈↓cial Intelligence.
␈↓ ↓N␈↓␈↓ ↓}␈↓↓Machine Intelligence 4␈↓, pp. 463-502 (eds    ␈↓ π∞␈↓What␈α~has␈α→been␈α~done:␈α→LCF,␈α~FOL,␈α→McCs
␈↓ ↓N␈↓␈↓ ↓}Meltzer, B. and Michie, D.). Edinburgh:     ␈↓ π∞␈↓epistemology and MTC.
␈↓ ↓N␈↓␈↓ ↓}Edinburgh University Press.
                                            ␈↓ π∞␈↓Who:␈α∪Weyhrauch,␈α∪JMC␈α∪part␈α∀time,␈α∪research
␈↓ ↓N␈↓␈↓αMcCarthy, J.␈↓ (1977a) Minimal Inference - A  ␈↓ π∞␈↓fellow␈αas␈αvisitor,␈α4␈αgraduate␈αstudents,␈α
disk␈α␈↓βC␈↓le,
␈↓ ↓N␈↓␈↓ ↓}New Way of Jumping to Conclusions (to       ␈↓ π∞␈↓terminals.
␈↓ ↓N␈↓␈↓ ↓}be published).
                                            ␈↓ π∞␈↓Publications:
␈↓ ↓N␈↓␈↓αMcCarthy, J.␈↓ (1977b) First Order Theories of
␈↓ ↓N␈↓␈↓ ↓}Individual Concepts (to be published).      ␈↓ π∞␈↓Recently␈α⊗Todd␈α⊗Wagner␈α⊗completed␈α↔a␈α⊗thesis
                                            ␈↓ π∞␈↓(Wagner␈α1977)␈αon␈αhardware␈αveri␈↓βC␈↓cation␈αusing
␈↓ ↓N␈↓␈↓αMcCarthy, J.␈↓ (1977c) Ascribing Mental       ␈↓ π∞␈↓FOL.␈α⊂ It␈α⊂turns␈α⊃out␈α⊂that␈α⊂almost␈α⊃all␈α⊂hardware
␈↓ ↓N␈↓␈↓ ↓}Qualities to Machines (to be published).    ␈↓ π∞␈↓veri␈↓βC␈↓cation␈α,has␈α+used␈α,simulation,␈α+and
                                            ␈↓ π∞␈↓simulation␈α∀can␈α∪never␈α∀be␈α∀complete.␈α∪ Wagner
␈↓ ↓N␈↓␈↓αMoore, Robert C.␈↓ (1977) Reasoning about     ␈↓ π∞␈↓has␈α⊂shown␈α⊂that␈α⊂proving␈α⊂hardware␈α⊃correct␈α⊂at
␈↓ ↓N␈↓␈↓ ↓}Knowledge and Action, ␈↓↓1977 IJCAI            ␈↓ π∞␈↓the␈α∞level␈α∞of␈α∞gates␈α∞and␈α∞␈↓βD␈↓ip-␈↓βD␈↓ops␈α∞is␈α∞well␈α∞suited
␈↓ ↓N␈↓↓␈↓ ↓}Proceedings␈↓.                                ␈↓ π∞␈↓to␈α∀proof-checking,␈α∀because␈α∀the␈α∃problems␈α∀of
                                            ␈↓ π∞␈↓mathematical␈α∞induction␈α
that␈α∞arise␈α∞in␈α
program
␈↓ ↓N␈↓␈↓αMcCarthy, J. ␈↓(1977d) First-Order            ␈↓ π∞␈↓veri␈↓βC␈↓cation usually don't arise.
␈↓ ↓N␈↓␈↓ ↓}Representation of Recursive Programs, (to
␈↓ ↓N␈↓␈↓ ↓}be published).                              ␈↓ π∞␈↓The␈α∨application␈α∨of␈α∨␈↓βC␈↓rst␈α∨order␈α∨logic␈α∨to
                                            ␈↓ π∞␈↓verifying␈αprograms␈α
has␈αbeen␈α
stimulated␈αby␈α
the
␈↓ ↓N␈↓Weyhrauch, FOL manual, fol proof collection,␈↓ π∞␈↓discovery␈α→(McCarthy␈α→1977c)␈α→that␈α→recursive
␈↓ ↓N␈↓␈↓ ↓}article on fol                              ␈↓ π∞␈↓programs␈αcan␈αbe␈αnicely␈αcharacterized␈αby␈αa␈α␈↓βC␈↓rst
                                            ␈↓ π∞␈↓order␈α∀functional␈α∪equation␈α∀and␈α∪a␈α∀␈↓βC␈↓rst␈α∪order
                                            ␈↓ π∞␈↓minimization␈α∩schema.␈α∩ Almost␈α∩all␈α⊃reasonable
                                            ␈↓ π∞␈↓extensional␈αproperties␈α
of␈αpure␈α
LISP␈αprograms
                                            ␈↓ π∞␈↓should␈αbe␈αconveniently␈αprovable.␈α We␈αpropose
                                            ␈↓ π∞␈↓to␈α∩investigate␈α∩these␈α⊃questions␈α∩further␈α∩in␈α⊃the
                                            ␈↓ π∞␈↓next time period.